Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    fact(X)  → if(zero(X),s(0),prod(X,fact(p(X))))
2:    add(0,X)  → X
3:    add(s(X),Y)  → s(add(X,Y))
4:    prod(0,X)  → 0
5:    prod(s(X),Y)  → add(Y,prod(X,Y))
6:    if(true,X,Y)  → X
7:    if(false,X,Y)  → Y
8:    zero(0)  → true
9:    zero(s(X))  → false
10:    p(s(X))  → X
There are 8 dependency pairs:
11:    FACT(X)  → IF(zero(X),s(0),prod(X,fact(p(X))))
12:    FACT(X)  → ZERO(X)
13:    FACT(X)  → PROD(X,fact(p(X)))
14:    FACT(X)  → FACT(p(X))
15:    FACT(X)  → P(X)
16:    ADD(s(X),Y)  → ADD(X,Y)
17:    PROD(s(X),Y)  → ADD(Y,prod(X,Y))
18:    PROD(s(X),Y)  → PROD(X,Y)
The approximated dependency graph contains 3 SCCs: {16}, {18} and {14}.
Tyrolean Termination Tool  (0.01 seconds)   ---  May 4, 2006